s:kl:KndIdLnk fp (IdTop) List, l:IdLnk, tg:Id.
sends-on-pair(s;l;tg)  (k:Knd. <k,l>  dom(s) & (tg  map(p.1of(p);s(<k,l>)))) 

latex

Definitions

t  T, x:A. B(x), Top, Id, x. t(x), 1of(t), map(f;as), S  T, IdLnkDeq, KindDeq, product-deq(A;B;a;b), deq-member(eq;x;L), b, Prop, A & B, x:A. B(x), false, , IdDeq, 2of(t), eqof(d), p  q, p  q, reduce(f;k;as), P  Q, P  Q, P & Q, P  Q, f(x), x  dom(f), a:A fp B(a), sends-on-pair(s;l;tg), IdLnk, Knd, (x  l), False, P  Q, True, A, b, T, Unit, ||as||, AB, , l[i], {T}

Lemmas

l member wf, iff functionality wrt iff, select wf, deq property, eqtt to assert, assert of band, and functionality wrt iff, eqff to assert, squash wf, bnot thru band, assert of bor, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, bnot wf, not wf, true wf, false wf, fpf wf, list-set-type, Knd wf, IdLnk wf, reduce wf, bor wf, band wf, eqof wf, pi2 wf, id-deq wf, bool wf, bfalse wf, assert wf, deq-member wf, product-deq wf, Kind-deq wf, idlnk-deq wf, Id wf, map wf, pi1 wf, top wf